1. $i$ : $\mathbb{N}$
\\[0ex]2. $f$ : \{$f$ $\mid$ $i$:\{$z$:$\mathbb{N}\mid$ $z$ $<$ $i$\}  $\rightarrow$ if ($i$ =$_{0}$ 0) then $\mathbb{Z}$ else \{$f$($i$ {-} 1)$\ldots\,$\} fi \}
\\[0ex]$\vdash$  $\forall$$j$:\{$k$:$\mathbb{N}\mid$ $k$ $<$ $i$\} . $f$($j$) $\in$ $\mathbb{Z}$